Techniques for determining whether two combinational designs are functionally different (which can be referred to as “combinational design discriminators” or CDDs) have a wide range of applications.
An example application of CDDs, within the area of ASIC design, is for EDA software that needs to determine whether two sequential designs are equivalent (which can be referred to as the “sequential equivalence problem”). In the sequential equivalence problem, the two designs to be compared can be referred to as the “reference” and “implementation” designs. More generally, the two designs to be compared can be referred to as a first compare design and a second compare design. An overview of known ASIC design flow is presented below. Next a known approach to solving the sequential equivalence problem is presented.
An Overview of Known ASIC Design Flow
Before proceeding further with the description, it may be helpful to place this process in context. FIG. 21 shows a simplified representation of an exemplary digital ASIC design flow. At a high level, the process starts with the product idea (step 2100) and is realized in an EDA software design process (step 2110). When the design is finalized, it can be taped-out (event 2140). After tape out, the fabrication process (step 2150) and packaging and assembly processes (step 2160) occur resulting, ultimately, in finished chips (result 2170).
The EDA software design process (step 2110) is actually composed of a number of steps 2112-2130, shown in linear fashion for simplicity. In an actual ASIC design process, the particular design might have to go back through steps until certain tests are passed. Similarly, in any actual design process, these steps may occur in different orders and combinations. This description is therefore provided by way of context and general explanation rather than as a specific, or recommended, design flow for a particular ASIC.
A brief description of the components steps of the EDA software design process (step 2110) will now be provided. The sequential equivalence problem can occur in step 2118 (“Netlist verification”), since this is when a designer can have a reference design (resulting from step 2114 “Logic design and functional verification”) and an implementation design (resulting from step 2116 “Synthesis and design for test”):                a) System design (step 2112): The designers describe the functionality that they want to implement; they can perform what-if planning to refine functionality, check costs, etc. Hardware-software architecture partitioning can occur at this stage. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include Model Architect, Saber, System Studio, and DesignWare® products.        b) Logic design and functional verification (step 2114): At this stage, the VHDL or Verilog code for modules in the system is written and the design is checked for functional accuracy. More specifically, the design is checked to ensure production of functionally correct outputs. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include VCS, VERA, DesignWare®, Magellan, Formality, ESP and LEDA products.        c) Synthesis and design for test (step 2116): Here, the VHDL/Verilog is translated to a netlist. The netlist can be optimized for the target technology. Additionally, the design and implementation of tests to permit checking of the finished chip occurs. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include Design Compiler®, Physical Compiler, Test Compiler, Power Compiler, FPGA Compiler, Tetramax, and DesignWare® products.        d) Netlist verification (step 2118): At this step, the netlist is checked for compliance with timing constraints and for correspondence with the VHDL/Verilog source code. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include Formality, PrimeTime, and VCS products.        e) Design planning (step 2120): Here, an overall floorplan for the chip is constructed and analyzed for timing and top-level routing. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include Astro and IC Compiler products.        f) Physical implementation (step 2122): The placement (positioning of circuit elements) and routing (connection of the same) occurs at this step. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include the Astro and IC Compiler products.        g) Analysis and extraction (step 2124): At this step, the circuit function is verified at a transistor level, this in turn permits what-if refinement. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include AstroRail, PrimeRail, Primetime, and Star RC/XT products.        h) Physical verification (step 2126): At this step various checking functions are performed to ensure correctness for: manufacturing, electrical issues, lithographic issues, and circuitry. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include the Hercules product.        i) Resolution enhancement (step 2128): This step involves geometric manipulations of the layout to improve manufacturability of the design. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include Proteus, ProteusAF, and PSMGen products.        j) Mask data preparation (step 2130): This step provides the “tape-out” data for production of masks for lithographic use to produce finished chips. Exemplary EDA software products from Synopsys, Inc. that can be used at this step include the CATS(R) family of products.        
An Example Approach to Solving the Sequential Equivalence Problem
For each of the first and second compare designs, a set of representative combinational sub-designs can be determined. The set of representative combinational sub-designs for the first compare design can be referred to as the “first combinational sub-designs” and the set of representative combinational designs for the second compare design can be referred to as the “second combinational sub-designs.”
As an example, a combinational sub-design can represent the next-state function for one bit of state, in either the first or second compare design.
A goal, in the solution of the sequential equivalence problem, can be for each member of the first combinational sub-designs to be paired with a corresponding member of the second combinational sub-designs. Each such pair of designs can be referred to as a “combinational design pair.” A process, by which combinational design pairs can be identified, with a CDD, can include the following steps. A subset of the first combinational sub-designs and a subset of the second combinational sub-designs can be combined to create an equivalence class (or “EC”). This EC, that can be referred to as “EC_for_CDD,” can be divided into smaller ECs by determining, with a CDD, that pairs of combinational designs, within EC_for_CDD, are functionally distinct. A goal of such subdivision can be to convert EC_for_CDD into a set of smaller ECs, where each of the smaller ECs is a combinational design pair.
Once all combinational design pairs have been identified, the potential equivalence, between the members of each such pair, can be addressed. If the members of a combinational design pair are equivalent, the pair can be referred to as an “equivalent combinational design pair.”
If all combinational design pairs are equivalent combinational design pairs, the first compare design and the second compare design are equivalent.
It is important to note that even if a particular CDD has placed two combinational designs in the same combinational design pair, it does not mean the combinational design pair, if processed for equivalence determination, will be found to represent equivalent functions. Unless one has gone to the computational effort of determining, positively, whether the members of a combinational design pair are in-fact equivalent, it can be the case that a better CDD can rule-out the same combinational design pair as a candidate for application to an equivalence determination process.
Therefore, while there are known methods of combinational design discrimination, there is a need for better methods of discriminating between combinational designs such that a more computationally expensive step (e.g., that of positive equivalence determination) can be avoided as often as possible.